/* 
 * Copyright 2014 Josef Hertl.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *      http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
package caetus.modelChecking.role;

import caetus.modelChecking.goal.ModelGoalMap;
import caetus.modelChecking.goal.ModelGoalSecret;
import caetus.modelChecking.variable.ModelBaseVariable;
import caetus.modelChecking.variable.ModelVariable;
import caetus.modelChecking.variable.ModelVariableType;
import caetus.pkcs11.tokenCapabilities.TokenCapabilities;
import java.util.LinkedList;
import java.util.List;

/**
 * Represents an actor. Further splits based on what the actor actually is - a
 * token or a person.
 *
 * @author Josef Hertl
 */
public abstract class ModelActor extends ModelRole {

    protected ModelVariable playedByAgent;

    public ModelActor(ModelVariable playedByAgent, String name, TokenCapabilities capabilities) {
        super(name, capabilities);
        this.playedByAgent = playedByAgent;
    }

    @Override
    public String makeRole() {
        String result = super.makeRoleStart();
        result += "played_by " + playedByAgent.getVariableName() + "\n";
        result += "def=\n\n";
        result += super.prepareLocalVariables();
        result += prepareInit();
        result += makeTransitions();
        result += super.makeRoleEnd();
        return result;
    }

    /**
     * Generates the transitions for the actor based off the variables and
     * capabilities it has.
     *
     * @return hlpsl-ready list of transitions including the "transition"
     * keyword.
     */
    protected abstract String makeTransitions();

    /**
     * Generates the local variables for the actor based off the token
     * capabilities. This should run before makeRole().
     */
    public abstract void generateLocalVariables();

    /**
     * Generates and sets the channels for this actor. Only one SND and RCV are
     * generated. The SND and RCV generated for this actor are actually
     * different channels from those returned. That is due to the fact that the
     * channels in session are named differently (SNDA, RCVA, SNDB, RCVB ...)
     * than those in the actors (always just SND and RCV)
     *
     * @return The two-element list containing one SND and one RCV channel. The
     * channels are returned so that they can later be included in the session
     * variable.
     */
    public List<ModelVariable> generateChannels() {
        globalVariables.add(new ModelBaseVariable("SND", ModelVariableType.CHANNEL));
        globalVariables.add(new ModelBaseVariable("RCV", ModelVariableType.CHANNEL));
        List<ModelVariable> resultList = new LinkedList<ModelVariable>();
        resultList.add(new ModelBaseVariable("SND" + playedByAgent.getVariableName(), ModelVariableType.CHANNEL));
        resultList.add(new ModelBaseVariable("RCV" + playedByAgent.getVariableName(), ModelVariableType.CHANNEL));
        return resultList;
    }

    /**
     * @param primed Defines if the incoming triggering variable is primed.
     * @return A string representation of the trigger that can be inserted into
     * the hlpsl model.
     */
    protected String makeTransitionTrigger(ModelVariable triggeringVariable, boolean primed) {
        String result = "RCV(" + triggeringVariable.getVariableName();
        if (primed) {
            result += "'";
        }
        result += ")";
        return result;
    }

    /**
     * @param triggeringText The constant that defines the input command, i.e.
     * encrypt_symmetric_lsk. It is never primed.
     * @param triggerArgument The data that is passed to the method that is
     * triggered by this command, i.e. data to be encrypted.
     * @return A string representation of the trigger that can be inserted into
     * the hlpsl model. This version primes the variable.
     */
    protected String makeTransitionTrigger(ModelVariable triggeringText, ModelVariable triggerArgument) {
        return "RCV(" + triggeringText.getVariableName() + "." + triggerArgument.getVariableName() + "')";
    }

    /**
     * State numbers: 0(LSK and LPK not set), 1(LSK set, LPK not set), 2(LSK not
     * set, LPK set), 3(both LSK and LPK set).
     *
     * @param stateNumber The required number of the state we want for this
     * transition
     * @return State = X, where X is the state number.
     */
    protected String makeStateCondition(int stateNumber) {
        return "State = " + stateNumber;
    }

    /**
     * @param stateNumberToSet The new state number.
     * @return State':= X, where X is the new state number.
     */
    protected String makeTransitionChangeState(int stateNumberToSet) {
        return "State':= " + stateNumberToSet;
    }

    /**
     * Makes an automated start trigger without any condition
     *
     * @return RCV(start)
     */
    protected String makeTransitionTriggerStart() {
        return "RCV(start)";
    }

    /**
     * @return =|> , including the line break afterwards
     */
    protected String makeTransitionArrow() {
        return " =|>\n";
    }

    /**
     * @return /\
     */
    protected String makeTransitionAND() {
        return " /\\ ";
    }

    /**
     * Prepares the SND part of a transition.
     *
     * @param sentVariable The variable that gets sent. Can be composed.
     * @param primed Shows if the variable is or is not primed.
     * @return SND(X) if not primed or SND(X') if primed
     */
    protected String makeTransitionSend(ModelVariable sentVariable, boolean primed) {
        String result = "SND(" + sentVariable.getVariableName();
        if (primed) {
            result += "'";
        }
        result += ")";
        return result;
    }

    /**
     * Simply wraps the input string in SND() and returns the transition. Does
     * NOT take priming into consideration.
     *
     * @param string The input to be wrapped with the SND( + )
     * @return SND(X), where X is the input string.
     */
    protected String makeTransitionSend(String string) {
        return "SND(" + string + ")";
    }

    /**
     * Prepares a transition to encrypt and send a variable.
     *
     * @param sentVariable The variable that gets sent.
     * @param primed Signals if the sent variable is primed or not.
     * @param encryptingVariable The variable used for encryption - usually a
     * key. It is never primed.
     * @return SND({sentVariable}_encryptingVariable)
     */
    protected String makeTransitionSendEcrypted(ModelVariable sentVariable, boolean primed, ModelVariable encryptingVariable) {
        String result = "SND({" + sentVariable.getVariableName();
        if (primed) {
            result += "'";
        }
        result += "}_" + encryptingVariable.getVariableName() + ")";
        return result;
    }

    /**
     * @return Transition that gives the input variable a fresh value.
     * Automatically primed.
     */
    protected String makeTransitionGenerate(ModelVariable generatedVariable) {
        return generatedVariable.getVariableName() + "' := new()";
    }

    /**
     * Finds and returns secret clause if the variable has one. the variable is
     * primed by default.
     *
     * @return null if the variable is not secret goal, secret clause otherwise.
     */
    protected String addSecretClauseToTransition(ModelBaseVariable secretVariable) {
        ModelGoalSecret secret = ModelGoalMap.findSecretOfVariable(secretVariable);
        if (secret != null) { //this should never be null, since encrypting value means it should be kept secret
            return secret.makeSecretClause(true);
        } else {
            return null;
        }
    }

    /**
     * Finds and returns secret clause if the variable has one. Allows setting
     * whether the variable is actually primed.
     *
     * @param primed Defines if the variable is primed.
     * @return null if the variable is not secret goal, secret clause otherwise.
     */
    protected String addSecretClauseToTransition(ModelBaseVariable secretVariable, boolean primed) {
        ModelGoalSecret secret = ModelGoalMap.findSecretOfVariable(secretVariable);
        if (secret != null) { //this should never be null, since encrypting value means it should be kept secret
            return secret.makeSecretClause(primed);
        } else {
            return null;
        }
    }

    public ModelVariable getPlayedByAgent() {
        return playedByAgent;
    }

    /**
     * A convenience method to quickly obtain the list of variables for the
     * session to "instantiate" this actor.
     *
     * @return List of the global variables this actor has WITHOUT the channels.
     */
    public List<ModelVariable> getGlobalVariableListNoChannels() {
        List<ModelVariable> resultList = new LinkedList<ModelVariable>();
        for (ModelVariable modelVariable : globalVariables) {
            if (!modelVariable.getVariableType().contains("channel")) {
                resultList.add(modelVariable);
            }
        }
        return resultList;
    }

    @Override
    protected String prepareInit() {
        return "\n";
    }
}
